Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

摘要

This paper positively solves an open problem if it is possible to provide aHilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard andLiu. To find a Hilbert system, we first introduce a sound, complete andcut-free tree (or nested) sequent calculus for EFL, which is an integratedcombination of Seligman's sequent calculus for basic hybrid logic and a treesequent calculus for modal logic. Then we translate a tree sequent into anordinary formula to specify a Hilbert system of EFL and finally show that ourHilbert system is sound and complete for the intended two-dimensionalsemantics.